Search Results

Documents authored by Lopez y Lopez, Fabiola

Found 5 Possible Name Variants:

Lopez, Hugo A.

Document
DOI: 10.4230/LIPIcs.ICLP.2010.270
Models for Trustworthy Service and Process Oriented Systems

Authors: Hugo A. Lopez

Published in: LIPIcs, Volume 7, Technical Communications of the 26th International Conference on Logic Programming (2010)

Abstract
Service and process-oriented systems promise to provide more effective business and work processes and more flexible and adaptable enterprise IT systems. However, the technologies and standards are still young and unstable, making research in their theoretical foundations increasingly important. Our studies focus on two dichotomies: the global/local views of service interactions, and their imperative/declarative specification. A global view of service interactions describes a process as a protocol for interactions, as e.g. an UML sequence diagram or a WS-CDL choreography. A local view describes the system as a set of processes, e.g. specified as a mipi-calculus or WS-BPEL process, implementing each participant in the process. While the global view is what is usually provided as specification, the local view is a necessary step towards a distributed implementation. If processes are defined imperatively, the control flow is defined explicitly, e.g. as a sequence or flow graph of interactions/commands. In a declarative approach processes are described as a collection of conditions they should fulfill in order to be considered correct. The two approaches have evolved rather independently from each other. Our thesis is that we can provide a theoretical framework based on typed concurrent process and concurrent constraint calculi for the specification, analysis and verification of service and process oriented system designs which bridges the global and local view and combines the imperative and declarative specification approaches, and can be employed to increase the trust in the developed systems. This article describes our main motivations, results and future research directions.
Cite as

Hugo A. Lopez. Models for Trustworthy Service and Process Oriented Systems. In Technical Communications of the 26th International Conference on Logic Programming. Leibniz International Proceedings in Informatics (LIPIcs), Volume 7, pp. 270-276, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{lopez:LIPIcs.ICLP.2010.270,
  author =	{Lopez, Hugo A.},
  title =	{{Models for Trustworthy Service and Process Oriented Systems}},
  booktitle =	{Technical Communications of the 26th International Conference on Logic Programming},
  pages =	{270--276},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-17-0},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{7},
  editor =	{Hermenegildo, Manuel and Schaub, Torsten},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICLP.2010.270},
  URN =		{urn:nbn:de:0030-drops-26073},
  doi =		{10.4230/LIPIcs.ICLP.2010.270},
  annote =	{Keywords: Concurrent Constraint Calculi, Session Types, Logic, Service and Process oriented computing}
}

Lopez, Carmen Torres

Document
Artifact
DOI: 10.4230/DARTS.5.2.4
Multiverse Debugging: Non-Deterministic Debugging for Non-Deterministic Programs (Artifact)

Authors: Robbert Gurdeep Singh, Carmen Torres Lopez, Stefan Marr, Elisa Gonzalez Boix, and Christophe Scholliers

Published in: DARTS, Volume 5, Issue 2, Special Issue of the 33rd European Conference on Object-Oriented Programming (ECOOP 2019)

Abstract
Many of today’s software systems are parallel or concurrent. With the rise of Node.js and more generally event-loop architectures, many systems need to handle concurrency. However, their non-deterministic behavior makes it hard to debug. Today’s interactive debuggers unfortunately do not support developers in debugging non-deterministic issues. They only allow exploring a single execution path. Therefore, some bugs may never be reproduced in the debugging session, because the conditions to trigger are not reached. As a solution, we propose multiverse debugging, a new approach for debugging non-deterministic programs that allow developers to observe all possible execution paths of a parallel program and debug it interactively. We introduce the concepts of multiverse breakpoints and stepping, which can halt a program in different execution paths, i.e. universes. We apply multiverse debugging to AmbientTalk, an actor-based language, resulting in Voyager, a proof of concept multiverse debugger that takes as input Featherweight AmbientTalk programs written in PLT-Redex, and allows programmers to interactively browse all possible execution states by means of multiverse breakpoints and stepping commands. We provide a proof of non-interference, i.e we prove that observing the behavior of a program by the debugger does not affect the behavior of that program and vice versa. Multiverse debugging establishes the foundation for debugging non-deterministic programs interactively, which we believe can aid the development of parallel and concurrent systems.
Cite as

Robbert Gurdeep Singh, Carmen Torres Lopez, Stefan Marr, Elisa Gonzalez Boix, and Christophe Scholliers. Multiverse Debugging: Non-Deterministic Debugging for Non-Deterministic Programs (Artifact). In Special Issue of the 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Dagstuhl Artifacts Series (DARTS), Volume 5, Issue 2, pp. 4:1-4:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@Article{singh_et_al:DARTS.5.2.4,
  author =	{Singh, Robbert Gurdeep and Lopez, Carmen Torres and Marr, Stefan and Boix, Elisa Gonzalez and Scholliers, Christophe},
  title =	{{Multiverse Debugging: Non-Deterministic Debugging for Non-Deterministic Programs}},
  pages =	{4:1--4:3},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2019},
  volume =	{5},
  number =	{2},
  editor =	{Singh, Robbert Gurdeep and Lopez, Carmen Torres and Marr, Stefan and Boix, Elisa Gonzalez and Scholliers, Christophe},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.5.2.4},
  URN =		{urn:nbn:de:0030-drops-107815},
  doi =		{10.4230/DARTS.5.2.4},
  annote =	{Keywords: Debugging, Concurrency, Actors, Formal Semantics}
}

Lopez, Aliaume

Document
DOI: 10.4230/LIPIcs.CSL.2021.32
Preservation Theorems Through the Lens of Topology

Authors: Aliaume Lopez

Published in: LIPIcs, Volume 183, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021)

Abstract
In this paper, we introduce a family of topological spaces that captures the existence of preservation theorems. The structure of those spaces allows us to study the relativisation of preservation theorems under suitable definitions of surjective morphisms, subclasses, sums, products, topological closures, and projective limits. Throughout the paper, we also integrate already known results into this new framework and show how it captures the essence of their proofs.
Cite as

Aliaume Lopez. Preservation Theorems Through the Lens of Topology. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 32:1-32:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{lopez:LIPIcs.CSL.2021.32,
  author =	{Lopez, Aliaume},
  title =	{{Preservation Theorems Through the Lens of Topology}},
  booktitle =	{29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
  pages =	{32:1--32:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-175-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{183},
  editor =	{Baier, Christel and Goubault-Larrecq, Jean},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.32},
  URN =		{urn:nbn:de:0030-drops-134660},
  doi =		{10.4230/LIPIcs.CSL.2021.32},
  annote =	{Keywords: Preservation theorem, Pre-spectral space, Noetherian space, Spectral space}
}
Document
DOI: 10.4230/LIPIcs.CSL.2018.29
Basic Operational Preorders for Algebraic Effects in General, and for Combined Probability and Nondeterminism in Particular

Authors: Aliaume Lopez and Alex Simpson

Published in: LIPIcs, Volume 119, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018)

Abstract
The "generic operational metatheory" of Johann, Simpson and Voigtländer (LiCS 2010) defines contextual equivalence, in the presence of algebraic effects, in terms of a basic operational preorder on ground-type effect trees. We propose three general approaches to specifying such preorders: (i) operational (ii) denotational, and (iii) axiomatic; coinciding with the three major styles of program semantics. We illustrate these via a nontrivial case study: the combination of probabilistic choice with nondeterminism, for which we show that natural instantiations of the three specification methods (operational in terms of Markov decision processes, denotational using a powerdomain, and axiomatic) all determine the same canonical preorder. We do this in the case of both angelic and demonic nondeterminism.
Cite as

Aliaume Lopez and Alex Simpson. Basic Operational Preorders for Algebraic Effects in General, and for Combined Probability and Nondeterminism in Particular. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 29:1-29:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{lopez_et_al:LIPIcs.CSL.2018.29,
  author =	{Lopez, Aliaume and Simpson, Alex},
  title =	{{Basic Operational Preorders for Algebraic Effects in General, and for Combined Probability and Nondeterminism in Particular}},
  booktitle =	{27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
  pages =	{29:1--29:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-088-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{119},
  editor =	{Ghica, Dan R. and Jung, Achim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.29},
  URN =		{urn:nbn:de:0030-drops-96965},
  doi =		{10.4230/LIPIcs.CSL.2018.29},
  annote =	{Keywords: contextual equivalence, algebraic effects, operational semantics, domain theory, nondeterminism, probabilistic choice, Markov decision process}
}
Document
DOI: 10.4230/LIPIcs.CSL.2017.24
Diagrammatic Semantics for Digital Circuits

Authors: Dan R. Ghica, Achim Jung, and Aliaume Lopez

Published in: LIPIcs, Volume 82, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017)

Abstract
We introduce a general diagrammatic theory of digital circuits, based on connections between monoidal categories and graph rewriting. The main achievement of the paper is conceptual, filling a foundational gap in reasoning syntactically and symbolically about a large class of digital circuits (discrete values, discrete delays, feedback). This complements the dominant approach to circuit modelling, which relies on simulation. The main advantage of our symbolic approach is the enabling of automated reasoning about parametrised circuits, with a potentially interesting new application to partial evaluation of digital circuits. Relative to the recent interest and activity in categorical and diagrammatic methods, our work makes several new contributions. The most important is establishing that categories of digital circuits are Cartesian and admit, in the presence of feedback expressive iteration axioms. The second is producing a general yet simple graph-rewrite framework for reasoning about such categories in which the rewrite rules are computationally efficient, opening the way for practical applications.
Cite as

Dan R. Ghica, Achim Jung, and Aliaume Lopez. Diagrammatic Semantics for Digital Circuits. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 24:1-24:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{ghica_et_al:LIPIcs.CSL.2017.24,
  author =	{Ghica, Dan R. and Jung, Achim and Lopez, Aliaume},
  title =	{{Diagrammatic Semantics for Digital Circuits}},
  booktitle =	{26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
  pages =	{24:1--24:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-045-3},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{82},
  editor =	{Goranko, Valentin and Dam, Mads},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.24},
  URN =		{urn:nbn:de:0030-drops-76715},
  doi =		{10.4230/LIPIcs.CSL.2017.24},
  annote =	{Keywords: digital circuits, monoidal categories, string diagrams, rewriting, operational semantics}
}

Lopez, Théodore

Document
DOI: 10.4230/LIPIcs.MFCS.2019.75
Determinisation of Finitely-Ambiguous Copyless Cost Register Automata

Authors: Théodore Lopez, Benjamin Monmege, and Jean-Marc Talbot

Published in: LIPIcs, Volume 138, 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)

Abstract
Cost register automata (CRA) are machines reading an input word while computing values using write-only registers: values from registers are combined using the two operations, as well as the constants, of a semiring. Particularly interesting is the subclass of copyless CRAs where the content of a register cannot be used twice for updating the registers. Originally deterministic, non-deterministic variant of CRA may also be defined: the semantics is then obtained by combining the values of all accepting runs with the additive operation of the semiring (as for weighted automata). We show that finitely-ambiguous copyless non-deterministic CRAs (i.e. the ones that admit a bounded number of accepting runs on every input word) can be effectively transformed into an equivalent copyless (deterministic) CRA, without requiring any specific property on the semiring. As a corollary, this also shows that regular look-ahead can effectively be removed from copyless CRAs.
Cite as

Théodore Lopez, Benjamin Monmege, and Jean-Marc Talbot. Determinisation of Finitely-Ambiguous Copyless Cost Register Automata. In 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 138, pp. 75:1-75:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{lopez_et_al:LIPIcs.MFCS.2019.75,
  author =	{Lopez, Th\'{e}odore and Monmege, Benjamin and Talbot, Jean-Marc},
  title =	{{Determinisation of Finitely-Ambiguous Copyless Cost Register Automata}},
  booktitle =	{44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)},
  pages =	{75:1--75:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-117-7},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{138},
  editor =	{Rossmanith, Peter and Heggernes, Pinar and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2019.75},
  URN =		{urn:nbn:de:0030-drops-110190},
  doi =		{10.4230/LIPIcs.MFCS.2019.75},
  annote =	{Keywords: Cost-register automata, Look-ahead removal, Unambiguity, Determinisation}
}

Lopez, Raphael

Document
DOI: 10.4230/LIPIcs.OPODIS.2019.19
Toward Linearizability Testing for Multi-Word Persistent Synchronization Primitives

Authors: Diego Cepeda, Sakib Chowdhury, Nan Li, Raphael Lopez, Xinzhe Wang, and Wojciech Golab

Published in: LIPIcs, Volume 153, 23rd International Conference on Principles of Distributed Systems (OPODIS 2019)

Abstract
Persistent memory makes it possible to recover in-memory data structures following a failure instead of rebuilding them from state saved in slow secondary storage. Implementing such recoverable data structures correctly is challenging as their underlying algorithms must deal with both parallelism and failures, which makes them especially susceptible to programming errors. Traditional proofs of correctness should therefore be combined with other methods, such as model checking or software testing, to minimize the likelihood of uncaught defects. This research focuses specifically on the algorithmic principles of software testing, particularly linearizability analysis, for multi-word persistent synchronization primitives such as conditional swap operations. We describe an efficient decision procedure for linearizability in this context, and discuss its practical applications in detecting previously-unknown bugs in implementations of multi-word persistent primitives.
Cite as

Diego Cepeda, Sakib Chowdhury, Nan Li, Raphael Lopez, Xinzhe Wang, and Wojciech Golab. Toward Linearizability Testing for Multi-Word Persistent Synchronization Primitives. In 23rd International Conference on Principles of Distributed Systems (OPODIS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 153, pp. 19:1-19:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{cepeda_et_al:LIPIcs.OPODIS.2019.19,
  author =	{Cepeda, Diego and Chowdhury, Sakib and Li, Nan and Lopez, Raphael and Wang, Xinzhe and Golab, Wojciech},
  title =	{{Toward Linearizability Testing for Multi-Word Persistent Synchronization Primitives}},
  booktitle =	{23rd International Conference on Principles of Distributed Systems (OPODIS 2019)},
  pages =	{19:1--19:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-133-7},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{153},
  editor =	{Felber, Pascal and Friedman, Roy and Gilbert, Seth and Miller, Avery},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2019.19},
  URN =		{urn:nbn:de:0030-drops-118050},
  doi =		{10.4230/LIPIcs.OPODIS.2019.19},
  annote =	{Keywords: Shared memory, persistent memory, synchronization, multi-word primitives, concurrency, correctness, software testing}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact